Inversion

Syntax directed means for each type, there’s only rule that can introduce it. E.g. the only way to introduce the plus syntax is using the PLUS rule.

We call these inversion lemmata:

Can be proven by (but doesn’t need to proven in exam):

• Proof by Induction
• Inspection

Weakening

Adding unrelated variables to the environment should not affect typing. Holds for most programming languages.

If you end up with two different environments, you can use weakening.

Substitution

Substitution is a [[meta-theoretic operation]].

Barendregt Convention

We assume that everything has been alpha renamed already so this doesn’t happen. Basically we just assume this won’t be a problem.

Substitution Lemma

To ensure substitution plays nicely with our language:

Related Reading

• 2025-09-30 Statics
• Substitution Practice